(set-option :produce-models true)
(set-logic QF_LIA)
(define-fun T ((%init Bool) ($left$0 Int) ($right$0 Int) ($head$0 Int) ($write$0 Int) ($move$0 Int) ($state$0 Int) ($cex$0 Bool) ($left$1 Int) ($right$1 Int) ($head$1 Int) ($write$1 Int) ($move$1 Int) ($state$1 Int) ($cex$1 Bool)) Bool 
    (and (= $left$1 (ite %init 0 (ite (= $state$0 0) $left$0 (ite (= $move$1 0) (div $left$0 10) (+ (* 10 $left$0) $write$1))))) 
         (= $head$1 (ite %init 0 (ite (= $state$0 0) $head$0 (ite (= $move$1 0) (mod $left$0 10) (mod $right$0 10))))) 
         (= $right$1 (ite %init 0 (ite (= $state$0 0) $right$0 (ite (= $move$1 0) (+ (* 10 $right$0) $write$1) (div $right$0 10)))))
         (= $write$1 (ite %init 0 (ite (and (= $state$0 1) (= $head$0 0)) 1 (ite (and (= $state$0 1) (= $head$0 1)) 1 (ite (and (= $state$0 2) (= $head$0 0)) 1 (ite (and (= $state$0 2) (= $head$0 1)) 0 (ite (and (= $state$0 3) (= $head$0 0)) 1 (ite (and (= $state$0 3) (= $head$0 1)) 1 (ite (and (= $state$0 4) (= $head$0 0)) 1 (ite (and (= $state$0 4) (= $head$0 1)) 0 0)))))))))) 
         (= $move$1 (ite %init 0 (ite (and (= $state$0 1) (= $head$0 0)) 1 (ite (and (= $state$0 1) (= $head$0 1)) 0 (ite (and (= $state$0 2) (= $head$0 0)) 0 (ite (and (= $state$0 2) (= $head$0 1)) 0 (ite (and (= $state$0 3) (= $head$0 0)) 1 (ite (and (= $state$0 3) (= $head$0 1)) 0 (ite (and (= $state$0 4) (= $head$0 0)) 1 (ite (and (= $state$0 4) (= $head$0 1)) 1 0)))))))))) (= $state$1 (ite %init 1 (ite (and (= $state$0 1) (= $head$0 0)) 2 (ite (and (= $state$0 1) (= $head$0 1)) 2 (ite (and (= $state$0 2) (= $head$0 0)) 1 (ite (and (= $state$0 2) (= $head$0 1)) 3 (ite (and (= $state$0 3) (= $head$0 0)) 0 (ite (and (= $state$0 3) (= $head$0 1)) 4 (ite (and (= $state$0 4) (= $head$0 0)) 4 (ite (and (= $state$0 4) (= $head$0 1)) 1 0)))))))))) (= $cex$1 (not (= $state$1 0)))))

(declare-fun %init () Bool)
(declare-fun $left$~1 () Int)
(declare-fun $right$~1 () Int)
(declare-fun $head$~1 () Int)
(declare-fun $write$~1 () Int)
(declare-fun $move$~1 () Int)
(declare-fun $state$~1 () Int)
(declare-fun $cex$~1 () Bool)
(assert (and (<= 0 $move$~1) (<= $move$~1 1)))
(assert (and (<= 0 $state$~1) (<= $state$~1 4)))
(declare-fun $left$0 () Int)
(declare-fun $right$0 () Int)
(declare-fun $head$0 () Int)
(declare-fun $write$0 () Int)
(declare-fun $move$0 () Int)
(declare-fun $state$0 () Int)
(declare-fun $cex$0 () Bool)
(assert (and (<= 0 $move$0) (<= $move$0 1)))
(assert (and (<= 0 $state$0) (<= $state$0 4)))
(assert (T %init $left$~1 $right$~1 $head$~1 $write$~1 $move$~1 $state$~1 $cex$~1 $left$0 $right$0 $head$0 $write$0 $move$0 $state$0 $cex$0))

(push 1)
(assert (not (=> true $cex$0)))
(check-sat)
(pop 1)

(declare-fun $left$1 () Int)
(declare-fun $right$1 () Int)
(declare-fun $head$1 () Int)
(declare-fun $write$1 () Int)
(declare-fun $move$1 () Int)
(declare-fun $state$1 () Int)
(declare-fun $cex$1 () Bool)
(assert (and (<= 0 $move$1) (<= $move$1 1)))
(assert (and (<= 0 $state$1) (<= $state$1 4)))
(assert (T false $left$0 $right$0 $head$0 $write$0 $move$0 $state$0 $cex$0 $left$1 $right$1 $head$1 $write$1 $move$1 $state$1 $cex$1))

(push 1)
(assert (not (=> $cex$0 $cex$1)))
(check-sat)
(pop 1)

(declare-fun $left$2 () Int)
(declare-fun $right$2 () Int)
(declare-fun $head$2 () Int)
(declare-fun $write$2 () Int)
(declare-fun $move$2 () Int)
(declare-fun $state$2 () Int)
(declare-fun $cex$2 () Bool)
(assert (and (<= 0 $move$2) (<= $move$2 1)))
(assert (and (<= 0 $state$2) (<= $state$2 4)))
(assert (T false $left$1 $right$1 $head$1 $write$1 $move$1 $state$1 $cex$1 $left$2 $right$2 $head$2 $write$2 $move$2 $state$2 $cex$2))

(push 1)
(assert (not (=> (and $cex$0 $cex$1) $cex$2)))
(check-sat)
(pop 1)

(declare-fun $left$3 () Int)
(declare-fun $right$3 () Int)
(declare-fun $head$3 () Int)
(declare-fun $write$3 () Int)
(declare-fun $move$3 () Int)
(declare-fun $state$3 () Int)
(declare-fun $cex$3 () Bool)
(assert (and (<= 0 $move$3) (<= $move$3 1)))
(assert (and (<= 0 $state$3) (<= $state$3 4)))
(assert (T false $left$2 $right$2 $head$2 $write$2 $move$2 $state$2 $cex$2 $left$3 $right$3 $head$3 $write$3 $move$3 $state$3 $cex$3))
(assert (not (=> (and $cex$0 $cex$1 $cex$2) $cex$3)))

(check-sat)

